 # STP (Simple Theorem Prover) top level makefile
 #
 # To make in debug mode, type 'make "OPTIMIZE=-g"
 # To make in optimized mode, type 'make "OPTIMIZE=-O3" 
 #
 # If you modify this file, be sure you're changing the version in
 # scripts/Makefile.in. The version at the top level stp directory
 # is automatically copied from there.

TOP=.
include  $(TOP)/scripts/Makefile.common

BIN_DIR=$(PREFIX)/bin
LIB_DIR=$(PREFIX)/lib
INCLUDE_DIR=$(PREFIX)/include/stp

SRC=src
BINARIES=bin/stp
LIBRARIES=lib/libstp.a
HEADERS=$(SRC)/c_interface/*.h

.PHONY: all
all: bin/stp lib/libstp.a
	@echo ""
	@echo "Compilation successful."
	@echo "Type 'make install' to install STP."

# An up-to-date $(SRC)/X/libX.a file also means that its constituent
# object files are also up-to-date: the following rules use this fact to
# remake only when necessary.

bin/stp: $(SRC)/main/main.o lib/libstp.a
	mkdir -p $(@D)
	$(CXX) $(CXXFLAGS) $(LDFLAGS) $^ -o $@

lib/libstp.a: $(addprefix $(SRC)/, \
		AST/libast.a STPManager/libstpmgr.a printer/libprinter.a \
		absrefine_counterexample/libabstractionrefinement.a \
		to-sat/libtosat.a sat/libminisat.a simplifier/libsimplifier.a \
		extlib-constbv/libconstantbv.a extlib-abc/libabc.a \
		c_interface/libcinterface.a parser/libparser.a main/libmain.a)
	mkdir -p $(@D)
	$(RM) $@
	$(call arcat,$@,$^)

# During the build of AST some classes are built that most of the other
# classes depend upon. So in a parallel make, AST should be made first.
$(addprefix $(SRC)/, \
	STPManager/libstpmgr.a printer/libprinter.a \
	absrefine_counterexample/libabstractionrefinement.a \
	to-sat/libtosat.a simplifier/libsimplifier.a c_interface/libcinterface.a \
	extlib-constbv/libconstantbv.a extlib-abc/libabc.a parser/libparser.a \
	main/libmain.a main/main.o): $(SRC)/AST/libast.a

$(SRC)/sat/libminisat.a: MAKEGOALS=core

# main.o is automatically built alongside libmain.a
$(SRC)/main/main.o : $(SRC)/main/libmain.a ;

$(SRC)/%: FORCE
	$(MAKE) -C $(@D) $(MAKEGOALS)
FORCE:

####

.PHONY: install
install: all
	@mkdir -p $(BIN_DIR)
	@mkdir -p $(LIB_DIR)
	@mkdir -p $(INCLUDE_DIR)
	@cp -f $(BINARIES) $(BIN_DIR)
	@cp -f $(LIBRARIES) $(LIB_DIR)
	@cp -f $(HEADERS) $(INCLUDE_DIR)
	@echo "STP installed successfully."

.PHONY: clean
clean:
	rm -rf *~ scripts/*~
	rm -rf *.a
	rm -rf lib/*.a
	rm -rf test/*~
	rm -rf bin/*~
	rm -rf bin/stp
	rm -rf *.log
	rm -f TAGS
	$(MAKE) clean -C $(SRC)/AST
	$(MAKE) clean -C $(SRC)/STPManager	
	$(MAKE) clean -C $(SRC)/printer
	$(MAKE) clean -C $(SRC)/extlib-constbv
	$(MAKE) clean -C $(SRC)/simplifier
	$(MAKE) clean -C $(SRC)/absrefine_counterexample
	$(MAKE) clean -C $(SRC)/to-sat
	$(MAKE) clean -C $(SRC)/sat
	$(MAKE) clean -C $(SRC)/c_interface	
	$(MAKE) clean -C $(SRC)/parser
	$(MAKE) clean -C $(SRC)/main
	$(MAKE) clean -C tests/c-api-tests

.PHONY: distclean configclean
distclean configclean: clean
	$(RM) scripts/config.info Makefile

.PHONY: regressall
regressall: all
	$(MAKE) check
	$(MAKE) regresscvc
	$(MAKE) regresssmt
	$(MAKE) regresssyn 
	$(MAKE) regresssmtcomp2007 
	$(MAKE) regressbigarray
	$(MAKE) regressstp
	$(MAKE) regressbio
	$(MAKE) regresseric
	$(MAKE) regresshistar
	$(MAKE) regresscrypto
	$(MAKE) unit_test
	$(MAKE) regresscapi


# Checks that simplifications are working.
.PHONY: unit_test
unit_test:
	cd unit_test ; ./unit_test.sh

# Runs the basic tests in tests/
.PHONY: check
check:
	$(MAKE) regresscvcbasic && $(MAKE) regresssmtbasic

#A generic test target called by the other tests.
.PHONY: baseTest
baseTest:
	@echo "*********************************************************" \
          | tee -a $(REGRESS_LOG)
	@echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
	@echo "*********************************************************" \
          | tee -a $(REGRESS_LOG)
	$(TO_RUN) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
	@echo "*********************************************************" \
          | tee -a $(REGRESS_LOG)
	@echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
	@echo "*********************************************************" \
          | tee -a $(REGRESS_LOG)


.PHONY: regresscvc
regresscvc: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)test/
regresscvc: REGRESS_LOG=`date +%Y-%m-%d`"-regress-cvc.log"
regresscvc: baseTest

.PHONY: regressbio
regressbio: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)bio-tests/
regressbio: REGRESS_LOG=`date +%Y-%m-%d`"-regress-bio.log"
regressbio: baseTest

.PHONY: regresscrypto
regresscrypto: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)crypto-tests/
regresscrypto: REGRESS_LOG=`date +%Y-%m-%d`"-regress-crypto.log"
regresscrypto: baseTest

.PHONY: regresssyn
regresssyn: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)synthesis-tests/
regresssyn: REGRESS_LOG = `date +%Y-%m-%d`"-regress-syn.log"
regresssyn: baseTest

.PHONY: regresssmtcomp2007
regresssmtcomp2007 : TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)smtcomp2007/
regresssmtcomp2007 : REGRESS_LOG = `date +%Y-%m-%d`"-regress-smtcomp2007.log"
regresssmtcomp2007 : baseTest

.PHONY: regresseric
regresseric: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)eric-test/
regresseric: REGRESS_LOG = `date +%Y-%m-%d`"-regress-eric.log"
regresseric: baseTest

.PHONY: regresshistar
regresshistar: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)histar-big-tests/
regresshistar: REGRESS_LOG = `date +%Y-%m-%d`"-regress-histar-big-tests.log"
regresshistar: baseTest


.PHONY: regressbigarray
regressbigarray: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)bigarray-test/
regressbigarray: REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log"
regressbigarray: baseTest

.PHONY: regresssmt
regresssmt: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)smt-test/
regresssmt: REGRESS_LOG = `date +%Y-%m-%d`"-regress-smt.log"
regresssmt: baseTest

.PHONY: regresscloud9
regresscloud9: TO_RUN=scripts/run_tests.pl --td=$(TEST_PREFIX)cloud9/
regresscloud9: REGRESS_LOG = `date +%Y-%m-%d`"-regress-cloud9.log"
regresscloud9: baseTest


.PHONY: regresscapi
regresscapi: TO_RUN=$(MAKE) -C tests/c-api-tests
regresscapi: REGRESS_LOG = `date +%Y-%m-%d`"-regress-c-api.log"
regresscapi: baseTest

.PHONY: regressstp
regressstp: TO_RUN=scripts/run_tests.pl --td=tests/big-test
regressstp: REGRESS_LOG = `date +%Y-%m-%d`"-regress-stp.log"
regressstp: baseTest

.PHONY: regresscvcbasic
regresscvcbasic: TO_RUN=scripts/run_tests.pl --td=tests/sample-tests
regresscvcbasic: REGRESS_LOG = `date +%Y-%m-%d`"-regress-cvcbasic.log"
regresscvcbasic: baseTest

.PHONY: regresssmtbasic
regresssmtbasic: TO_RUN=scripts/run_tests.pl --td=tests/sample-smt-tests
regresssmtbasic: REGRESS_LOG = `date +%Y-%m-%d`"-regress-smtbasic.log"
regresssmtbasic: baseTest



# The higher the level, the more tests are run (3 = all)
REGRESS_LEVEL=4
REGRESS_TESTS=$(REGRESS_TESTS0)
PROGNAME=bin/stp
ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
GRIND_LOG = `date +%Y-%m-%d`"-grind.log"
GRINDPROG = valgrind --leak-check=full --undef-value-errors=no
GRIND_TAR  = $(BIN_DIR)/stp -d
GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" 
GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS)
.PHONY: grind
grind:

	$(MAKE) install CFLAGS="-ggdb -pg -g"
	@echo "*********************************************************" \
          | tee -a $(GRIND_LOG)
	@echo "Starting tests at" `date` | tee -a $(GRIND_LOG)
	@echo "*********************************************************" \
          | tee -a $(GRIND_LOG)
	scripts/run_cvc_tests.pl $(GRIND_OPTIONS) 2>&1 | tee -a $(GRIND_LOG);eval [ $${PIPESTATUS[0]} -eq 0 ]
	@echo "*********************************************************" \
          | tee -a $(GRIND_LOG)
	@echo "Output is saved in $(GRIND_LOG)" | tee -a $(GRIND_LOG)
	@echo "*********************************************************" \
          | tee -a $(GRIND_LOG)
